Validate project files, add order, insert version#116
Conversation
There was a problem hiding this comment.
what's these day the recommended way of automatically follow stable releases? the file leanweb-build.sh contains lake update -R this will not be good enough to automatically update to v4.30.0, v4.31.0, ... when they are released, will it?
There was a problem hiding this comment.
For live.lean-lang.org, we're currently getting the stable release by following the cslib stable tag: we literally
curl -L https://raw.githubusercontent.com/leanprover/cslib/stable/lean-toolchain | tee lean-toolchain
But this doesn't work for "latest release" where there's no corresponding tag in mathlib or cslib, and it doesn't work as soon as you want to say "I want the latest stable release where there's a version of cslib, and lean4export, and comparator"... which is also something I want. So I'm planning on doing something a bit more complicated, I can try upstreaming if it would be helpful because there's not currently a great answer here.
There was a problem hiding this comment.
ok that sounds even hackier indeed.
I'm going to revert that for this PR, but I'd be happy to have a look at that in another PR seperately.
Ideally lake would provide an official way for projects to update to the latest stable Lean release, something like lake update --stable. Currently, to my best knowledge, the "most official" way to follow stable Lean is setting the toolchain to stable. Therefore, I would like to keep that in this demo project.
|
I've put all these suggestions into a commit (including fixing the tests and adding doc). It seems you've disabled pushing to the PR branch for reviewers, so it is here: I've also added a second commit reverting the toolchain to stable and fixing the build script to update the stable toolchain. Less sure about this. I would like a way so that running the .sh script automatically updates the project to the latest stable Lean release. If you have insider knowledge how to do this correctly, please feel free to update the bash script Feel free to take these commits as you agree and leave out parts where you don't think that's on the line of your PR. |
Copy of #116 by [Robert J. Simmons](https://github.com/robsimmons) because I don't have push access to the original PR branch in order to fix the tests. Makes a few changes to the project validation structure. - uses Zod parsing to take care of remaining to-dos around validating project configurations - adds a sort order field that allows the frontend to order projects by a custom sort - Allows project names to use templating: - `_Vers_` will get replaced by the toolchain (e.g. `v4.30.0`) or by `Lean` if the toolchain format isn't recognized and - `_LeanVers_` will get replaced by the toolchain plus "Lean" (e.g. `Lean v4.30.0`) or by `Lean` if the toolchain format isn't recognized Co-authored-by: Rob Simmons <rob@lean-fro.org>
|
Thanks Rob for the PR! I created and merged a copy of this PR at #122, since I wanted to push a couple of fixes (fixing tests; reverting to stable toolchain - see above) before merging. This is a setting the PR creator could enable: to allow maintainers of the repo to push directly to the PR branch. I'm looking forward to see more fixes and features from you :) |
2 participants
Makes a few changes to the project validation structure.
_Vers_will get replaced by the toolchain (e.g.v4.30.0) or byLeanif the toolchain format isn't recognized and_LeanVers_will get replaced by the toolchain plus "Lean" (e.g.Lean v4.30.0) or byLeanif the toolchain format isn't recognized